Left Termination of the query pattern
balance(g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

balance(T, TB) :- balance55(T, XX0, XX1, [], .(','(nil, -(XX0, XX0)), XX1), [], .(','(TB, -(I, [])), X), X, I, []).
balance55(nil, C, T, T, A, B, A, B, X, X).
balance55(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT) :- ','(balance55(L, XX0, XX1, .(','(nil, -(XX2, XX2)), XX3), HR1, TR1, H, T, IH, .(V, IT1)), balance55(R, XX2, XX3, NT, HR, TR, HR1, TR1, IT1, IT)).
balance5(nil, C, T, T, A, B, A, B, X, X) :- balance55(nil, C, T, T, A, B, A, B, X, X).
balance5(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT) :- balance55(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT).
balance(nil, -(X, X), -(A, B), -(A, B), -(.(','(nil, -(C, C)), T), T)) :- balance5(nil, C, T, T, A, B, A, B, X, X).
balance(tree(L, V, R), -(IH, IT), -(.(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T))), -(HR, TR), -(.(','(nil, -(XX0, XX0)), XX1), NT)) :- balance5(tree(L, V, R), XX0, XX1, NT, HR, TR, .(','(tree(LB, VB, RB), -(A, D)), H), .(','(LB, -(A, .(VB, X))), .(','(RB, -(X, D)), T)), IH, IT).

Query: balance(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="D: balance(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: balance(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, [])\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, []), SCOPE: 2, CLAUSE: 1 | balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, []), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, []), SCOPE: 2, CLAUSE: 1\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: balance55(T5, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(T7, -(X7, [])), X8), X8, X7, []), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX5 is free\nX6 is free\nX7 is free\nX8 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), balance55(T22, X115, X116, [], .(','(nil, -(X120, X120)), X121), [], X117, X118, X119, []))\n\nT20 is ground\nT21 is ground\nT22 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="C: balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119))\n\nT20 is ground\nT21 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="B: balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, [])\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), SCOPE: 3, CLAUSE: 1 | balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nT21 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), SCOPE: 3, CLAUSE: 1\n\nT20 is ground\nT21 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: balance55(T20, X120, X121, .(','(nil, -(X115, X115)), X116), X117, X118, .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)), T26, T27, .(T21, X119)), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nT21 is ground\nX120 is free\nX121 is free\nX115 is free\nX116 is free\nX117 is free\nX118 is free\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(balance55(T139, X303, X304, .(','(nil, -(X298, X298)), X299), X300, X301, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, .(T140, X302)), balance55(T141, X298, X299, .(','(nil, -(X305, X305)), X306), X307, X308, X300, X301, X302, .(T152, X309)))\n\nT139 is ground\nT140 is ground\nT141 is ground\nT152 is ground\nX303 is free\nX304 is free\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free\nX298 is free\nX299 is free\nX300 is free\nX301 is free\nX302 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: balance55(T139, X303, X304, .(','(nil, -(X298, X298)), X299), X300, X301, .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))), T153, T154, .(T140, X302))\n\nT139 is ground\nT140 is ground\nX303 is free\nX304 is free\nX298 is free\nX299 is free\nX300 is free\nX301 is free\nX302 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="A: balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309))\n\nT141 is ground\nT152 is ground\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309)), SCOPE: 4, CLAUSE: 1 | balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309)), SCOPE: 4, CLAUSE: 2\n\nT141 is ground\nT152 is ground\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309)), SCOPE: 4, CLAUSE: 1\n\nT141 is ground\nT152 is ground\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: balance55(T141, T186, T187, .(','(nil, -(X305, X305)), X306), X307, X308, T188, T189, T190, .(T152, X309)), SCOPE: 4, CLAUSE: 2\n\nT141 is ground\nT152 is ground\nX305 is free\nX306 is free\nX307 is free\nX308 is free\nX309 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(balance55(T306, T321, T322, .(','(nil, -(X472, X472)), X473), X474, X475, T323, T324, T325, .(T307, X476)), balance55(T308, X472, X473, .(','(nil, -(X477, X477)), X478), X479, X480, X474, X475, X476, .(T320, X481)))\n\nT306 is ground\nT307 is ground\nT308 is ground\nT320 is ground\nX477 is free\nX478 is free\nX479 is free\nX480 is free\nX481 is free\nX472 is free\nX473 is free\nX474 is free\nX475 is free\nX476 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: balance55(T306, T321, T322, .(','(nil, -(X472, X472)), X473), X474, X475, T323, T324, T325, .(T307, X476))\n\nT306 is ground\nT307 is ground\nX472 is free\nX473 is free\nX474 is free\nX475 is free\nX476 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: balance55(T308, T344, T345, .(','(nil, -(X477, X477)), X478), X479, X480, T346, T347, T348, .(T320, X481))\n\nT308 is ground\nT320 is ground\nX477 is free\nX478 is free\nX479 is free\nX480 is free\nX481 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, []), SCOPE: 5, CLAUSE: 1 | balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, []), SCOPE: 5, CLAUSE: 2\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, []), SCOPE: 5, CLAUSE: 1\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: balance55(T22, T50, T51, [], .(','(nil, -(T48, T48)), T49), [], T52, T53, T54, []), SCOPE: 5, CLAUSE: 2\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(balance55(T452, T468, T469, .(','(nil, -(X618, X618)), X619), X620, X621, T470, T471, T472, .(T453, X622)), balance55(T454, X618, X619, [], .(','(nil, -(T474, T474)), T473), [], X620, X621, X622, []))\n\nT452 is ground\nT453 is ground\nT454 is ground\nX618 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: balance55(T452, T468, T469, .(','(nil, -(X618, X618)), X619), X620, X621, T470, T471, T472, .(T453, X622))\n\nT452 is ground\nT453 is ground\nX618 is free\nX619 is free\nX620 is free\nX621 is free\nX622 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: balance55(T454, T493, T494, [], .(','(nil, -(T498, T498)), T499), [], T495, T496, T497, [])\n\nT454 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 44 [arrowhead = none ];
44 -> 2;

45 [label="ONLY EVAL with clause\nbalance(X3, X4) :- balance55(X3, X5, X6, [], .(','(nil, -(X5, X5)), X6), [], .(','(X4, -(X7, [])), X8), X8, X7, []).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> T7,\nX4 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 45 [arrowhead = none ];
45 -> 3;

46 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 46 [arrowhead = none ];
46 -> 4;

47 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 47 [arrowhead = none ];
47 -> 5;

48 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 48 [arrowhead = none ];
48 -> 6;

49 [label="EVAL with clause\nbalance55(nil, X37, X38, X38, X39, X40, X39, X40, X41, X41).\nand substitutionT5 -> nil,\nX5 -> [],\nX37 -> [],\nX6 -> [],\nX38 -> [],\nX43 -> [],\nX39 -> .(','(nil, -([], [])), []),\nX40 -> [],\nT7 -> nil,\nX7 -> [],\nX42 -> [],\nX8 -> [],\nX41 -> []", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 49 [arrowhead = none ];
49 -> 7;

50 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 50 [arrowhead = none ];
50 -> 8;

51 [label="EVAL with clause\nbalance55(tree(X97, X98, X99), X100, X101, X102, X103, X104, .(','(tree(X105, X106, X107), -(X108, X109)), X110), .(','(X105, -(X108, .(X106, X111))), .(','(X107, -(X111, X109)), X112)), X113, X114) :- ','(balance55(X97, X100, X101, .(','(nil, -(X115, X115)), X116), X117, X118, X110, X112, X113, .(X98, X119)), balance55(X99, X115, X116, X102, X103, X104, X117, X118, X119, X114)).\nand substitutionX97 -> T20,\nX98 -> T21,\nX99 -> T22,\nT5 -> tree(T20, T21, T22),\nX5 -> X120,\nX100 -> X120,\nX6 -> X121,\nX101 -> X121,\nX102 -> [],\nX103 -> .(','(nil, -(X120, X120)), X121),\nX104 -> [],\nX105 -> T28,\nX106 -> T29,\nX107 -> T31,\nT7 -> tree(T28, T29, T31),\nX7 -> T27,\nX108 -> T27,\nX109 -> [],\nX8 -> .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)),\nX110 -> .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)),\nX111 -> T30,\nX112 -> T26,\nX123 -> .(','(T28, -(T27, .(T29, T30))), .(','(T31, -(T30, [])), T26)),\nX113 -> T27,\nX114 -> [],\nX125 -> T26,\nX122 -> T27,\nT23 -> T28,\nT24 -> T29,\nX124 -> T30,\nT25 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 51 [arrowhead = none ];
51 -> 10;

52 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 52 [arrowhead = none ];
52 -> 11;

53 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 53 [arrowhead = none ];
53 -> 9;

54 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
10 -> 54 [arrowhead = none ];
54 -> 12;

55 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nreplacements:X120 -> T48,\nX121 -> T49,\nX115 -> T50,\nX116 -> T51,\nX117 -> T52,\nX118 -> T53,\nX119 -> T54", fontsize=14, style = filled, fillcolor = violet];
10 -> 55 [arrowhead = none ];
55 -> 13;

56 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 56 [arrowhead = none ];
56 -> 14;

57 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 57 [arrowhead = none ];
57 -> 34;

58 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 58 [arrowhead = none ];
58 -> 15;

59 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 59 [arrowhead = none ];
59 -> 16;

60 [label="EVAL with clause\nbalance55(nil, X214, X215, X215, X216, X217, X216, X217, X218, X218).\nand substitutionT20 -> nil,\nX120 -> X219,\nX214 -> X219,\nX121 -> .(','(nil, -(X221, X221)), X222),\nX215 -> .(','(nil, -(X221, X221)), X222),\nX115 -> X221,\nX116 -> X222,\nX220 -> .(','(nil, -(X221, X221)), X222),\nX117 -> .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)),\nX216 -> .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)),\nX118 -> T108,\nX217 -> T108,\nT28 -> T103,\nT27 -> .(T109, T110),\nT29 -> T105,\nT30 -> T106,\nT31 -> T107,\nT26 -> T108,\nX223 -> .(','(T103, -(.(T109, T110), .(T105, T106))), .(','(T107, -(T106, [])), T108)),\nX224 -> T108,\nX218 -> .(T109, T110),\nT21 -> T109,\nX119 -> T110,\nT104 -> .(T109, T110)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 60 [arrowhead = none ];
60 -> 17;

61 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 61 [arrowhead = none ];
61 -> 18;

62 [label="EVAL with clause\nbalance55(tree(X280, X281, X282), X283, X284, X285, X286, X287, .(','(tree(X288, X289, X290), -(X291, X292)), X293), .(','(X288, -(X291, .(X289, X294))), .(','(X290, -(X294, X292)), X295)), X296, X297) :- ','(balance55(X280, X283, X284, .(','(nil, -(X298, X298)), X299), X300, X301, X293, X295, X296, .(X281, X302)), balance55(X282, X298, X299, X285, X286, X287, X300, X301, X302, X297)).\nand substitutionX280 -> T139,\nX281 -> T140,\nX282 -> T141,\nT20 -> tree(T139, T140, T141),\nX120 -> X303,\nX283 -> X303,\nX121 -> X304,\nX284 -> X304,\nX115 -> X305,\nX116 -> X306,\nX285 -> .(','(nil, -(X305, X305)), X306),\nX117 -> X307,\nX286 -> X307,\nX118 -> X308,\nX287 -> X308,\nX288 -> T157,\nX289 -> T158,\nX290 -> T160,\nT28 -> tree(T157, T158, T160),\nT27 -> T154,\nX291 -> T154,\nT29 -> T161,\nT30 -> T156,\nX292 -> .(T161, T156),\nT31 -> T155,\nT26 -> .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)),\nX293 -> .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153))),\nX294 -> T159,\nX295 -> T153,\nT149 -> .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)),\nX296 -> T154,\nT21 -> T152,\nX119 -> X309,\nX297 -> .(T152, X309),\nT151 -> T153,\nT145 -> T154,\nT148 -> T155,\nT147 -> T156,\nT142 -> T157,\nT143 -> T158,\nT150 -> T159,\nT144 -> T160,\nT146 -> T161", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 62 [arrowhead = none ];
62 -> 20;

63 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 63 [arrowhead = none ];
63 -> 21;

64 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 64 [arrowhead = none ];
64 -> 19;

65 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
20 -> 65 [arrowhead = none ];
65 -> 22;

66 [label="SPLIT 2\nnew knowledge:\nT139 is ground\nreplacements:X303 -> T184,\nX304 -> T185,\nX298 -> T186,\nX299 -> T187,\nX300 -> T188,\nX301 -> T189,\nX302 -> T190", fontsize=14, style = filled, fillcolor = violet];
20 -> 66 [arrowhead = none ];
66 -> 23;

67 [label="INSTANCE with matching:\nT141 -> T139\nT186 -> X303\nT187 -> X304\nX305 -> X298\nX306 -> X299\nX307 -> X300\nX308 -> X301\nT188 -> .(','(T155, -(T156, [])), .(','(T157, -(T154, .(T158, T159))), .(','(T160, -(T159, .(T161, T156))), T153)))\nT189 -> T153\nT190 -> T154\nT152 -> T140\nX309 -> X302", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 67 [arrowhead = none , style=dashed];
67 -> 23[style=dashed];

68 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
23 -> 68 [arrowhead = none ];
68 -> 24;

69 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 69 [arrowhead = none ];
69 -> 25;

70 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 70 [arrowhead = none ];
70 -> 26;

71 [label="EVAL with clause\nbalance55(nil, X396, X397, X397, X398, X399, X398, X399, X400, X400).\nand substitutionT141 -> nil,\nT186 -> T267,\nX396 -> T267,\nT187 -> .(','(nil, -(T269, T269)), T270),\nX397 -> .(','(nil, -(T269, T269)), T270),\nX305 -> T269,\nX306 -> T270,\nT268 -> .(','(nil, -(T269, T269)), T270),\nX307 -> T271,\nX398 -> T271,\nX308 -> T272,\nX399 -> T272,\nT188 -> T271,\nX401 -> T271,\nT189 -> T272,\nX402 -> T272,\nT190 -> .(T274, T275),\nX400 -> .(T274, T275),\nT152 -> T274,\nX309 -> T275,\nT273 -> .(T274, T275)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 71 [arrowhead = none ];
71 -> 27;

72 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 72 [arrowhead = none ];
72 -> 28;

73 [label="EVAL with clause\nbalance55(tree(X454, X455, X456), X457, X458, X459, X460, X461, .(','(tree(X462, X463, X464), -(X465, X466)), X467), .(','(X462, -(X465, .(X463, X468))), .(','(X464, -(X468, X466)), X469)), X470, X471) :- ','(balance55(X454, X457, X458, .(','(nil, -(X472, X472)), X473), X474, X475, X467, X469, X470, .(X455, X476)), balance55(X456, X472, X473, X459, X460, X461, X474, X475, X476, X471)).\nand substitutionX454 -> T306,\nX455 -> T307,\nX456 -> T308,\nT141 -> tree(T306, T307, T308),\nT186 -> T321,\nX457 -> T321,\nT187 -> T322,\nX458 -> T322,\nX305 -> X477,\nX306 -> X478,\nX459 -> .(','(nil, -(X477, X477)), X478),\nX307 -> X479,\nX460 -> X479,\nX308 -> X480,\nX461 -> X480,\nX462 -> T311,\nX463 -> T312,\nX464 -> T313,\nX465 -> T314,\nX466 -> T315,\nX467 -> T323,\nT188 -> .(','(tree(T311, T312, T313), -(T314, T315)), T323),\nX468 -> T317,\nX469 -> T324,\nT189 -> .(','(T311, -(T314, .(T312, T317))), .(','(T313, -(T317, T315)), T324)),\nT190 -> T325,\nX470 -> T325,\nT152 -> T320,\nX309 -> X481,\nX471 -> .(T320, X481),\nT309 -> T321,\nT310 -> T322,\nT316 -> T323,\nT318 -> T324,\nT319 -> T325", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 73 [arrowhead = none ];
73 -> 30;

74 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 74 [arrowhead = none ];
74 -> 31;

75 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 75 [arrowhead = none ];
75 -> 29;

76 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
30 -> 76 [arrowhead = none ];
76 -> 32;

77 [label="SPLIT 2\nnew knowledge:\nT306 is ground\nreplacements:X472 -> T344,\nX473 -> T345,\nX474 -> T346,\nX475 -> T347,\nX476 -> T348", fontsize=14, style = filled, fillcolor = violet];
30 -> 77 [arrowhead = none ];
77 -> 33;

78 [label="INSTANCE with matching:\nT141 -> T306\nT186 -> T321\nT187 -> T322\nX305 -> X472\nX306 -> X473\nX307 -> X474\nX308 -> X475\nT188 -> T323\nT189 -> T324\nT190 -> T325\nT152 -> T307\nX309 -> X476", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 78 [arrowhead = none , style=dashed];
78 -> 23[style=dashed];

79 [label="INSTANCE with matching:\nT141 -> T308\nT186 -> T344\nT187 -> T345\nX305 -> X477\nX306 -> X478\nX307 -> X479\nX308 -> X480\nT188 -> T346\nT189 -> T347\nT190 -> T348\nT152 -> T320\nX309 -> X481", fontsize=14, style = filled, fillcolor = lightgrey];
33 -> 79 [arrowhead = none , style=dashed];
79 -> 23[style=dashed];

80 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 80 [arrowhead = none ];
80 -> 35;

81 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 81 [arrowhead = none ];
81 -> 36;

82 [label="EVAL with clause\nbalance55(nil, X554, X555, X555, X556, X557, X556, X557, X558, X558).\nand substitutionT22 -> nil,\nT50 -> T415,\nX554 -> T415,\nT51 -> [],\nX555 -> [],\nT416 -> [],\nT48 -> T417,\nT49 -> T418,\nX556 -> .(','(nil, -(T417, T417)), T418),\nX557 -> [],\nT52 -> .(','(nil, -(T417, T417)), T418),\nT53 -> [],\nT54 -> [],\nX558 -> [],\nT419 -> []", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 82 [arrowhead = none ];
82 -> 37;

83 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 83 [arrowhead = none ];
83 -> 38;

84 [label="EVAL with clause\nbalance55(tree(X600, X601, X602), X603, X604, X605, X606, X607, .(','(tree(X608, X609, X610), -(X611, X612)), X613), .(','(X608, -(X611, .(X609, X614))), .(','(X610, -(X614, X612)), X615)), X616, X617) :- ','(balance55(X600, X603, X604, .(','(nil, -(X618, X618)), X619), X620, X621, X613, X615, X616, .(X601, X622)), balance55(X602, X618, X619, X605, X606, X607, X620, X621, X622, X617)).\nand substitutionX600 -> T452,\nX601 -> T453,\nX602 -> T454,\nT22 -> tree(T452, T453, T454),\nT50 -> T468,\nX603 -> T468,\nT51 -> T469,\nX604 -> T469,\nX605 -> [],\nT48 -> T474,\nT49 -> T473,\nX606 -> .(','(nil, -(T474, T474)), T473),\nX607 -> [],\nX608 -> T459,\nX609 -> T460,\nX610 -> T461,\nX611 -> T462,\nX612 -> T463,\nX613 -> T470,\nT52 -> .(','(tree(T459, T460, T461), -(T462, T463)), T470),\nX614 -> T465,\nX615 -> T471,\nT53 -> .(','(T459, -(T462, .(T460, T465))), .(','(T461, -(T465, T463)), T471)),\nT54 -> T472,\nX616 -> T472,\nX617 -> [],\nT455 -> T468,\nT456 -> T469,\nT464 -> T470,\nT466 -> T471,\nT467 -> T472,\nT458 -> T473,\nT457 -> T474", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 84 [arrowhead = none ];
84 -> 40;

85 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 85 [arrowhead = none ];
85 -> 41;

86 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 86 [arrowhead = none ];
86 -> 39;

87 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
40 -> 87 [arrowhead = none ];
87 -> 42;

88 [label="SPLIT 2\nnew knowledge:\nT452 is ground\nreplacements:X618 -> T493,\nX619 -> T494,\nX620 -> T495,\nX621 -> T496,\nX622 -> T497,\nT474 -> T498,\nT473 -> T499", fontsize=14, style = filled, fillcolor = violet];
40 -> 88 [arrowhead = none ];
88 -> 43;

89 [label="INSTANCE with matching:\nT141 -> T452\nT186 -> T468\nT187 -> T469\nX305 -> X618\nX306 -> X619\nX307 -> X620\nX308 -> X621\nT188 -> T470\nT189 -> T471\nT190 -> T472\nT152 -> T453\nX309 -> X622", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 89 [arrowhead = none , style=dashed];
89 -> 23[style=dashed];

90 [label="INSTANCE with matching:\nT22 -> T454\nT50 -> T493\nT51 -> T494\nT48 -> T498\nT49 -> T499\nT52 -> T495\nT53 -> T496\nT54 -> T497", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 90 [arrowhead = none , style=dashed];
90 -> 13[style=dashed];

}

(2) Obligation:

Triples:

balance55A(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) :- balance55A(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25).
balance55A(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) :- ','(balance55cA(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25), balance55A(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)).
balance55B(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) :- balance55A(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21).
balance55B(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) :- ','(balance55cA(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21), balance55B(X3, X17, X18, X6, X7, X19, X20, X21)).
balanceD(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) :- balance55A(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21).
balanceD(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) :- ','(balance55cA(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21), balance55A(X3, X13, X14, X22, X23, X24, X25, X15, X16, X21, X4, X26)).
balanceD(tree(X1, X2, X3), tree(X4, X5, X6)) :- ','(balance55cC(X1, X7, X8, X9, X10, X11, X12, X4, X13, X5, X14, X6, X15, X2, X16), balance55B(X3, X9, X10, X7, X8, X11, X12, X16)).

Clauses:

balance55cA(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7).
balance55cA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) :- ','(balance55cA(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25), balance55cA(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)).
balance55cB(nil, X1, [], X2, X3, .(','(nil, -(X2, X2)), X3), [], []).
balance55cB(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) :- ','(balance55cA(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21), balance55cB(X3, X17, X18, X6, X7, X19, X20, X21)).
balance55cC(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6).
balance55cC(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20) :- ','(balance55cA(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25), balance55cA(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)).

Afs:

balanceD(x1, x2)  =  balanceD(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
balanceD_in: (b,f)
balance55A_in: (b,f,f,f,f,f,f,f,f,f,b,f)
balance55cA_in: (b,f,f,f,f,f,f,f,f,f,b,f)
balance55cC_in: (b,f,f,f,f,f,f,f,f,f,f,f,f,b,f)
balance55B_in: (b,f,f,f,f,f,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → U7_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55A_in_gaaaaaaaaaga(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21))
BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21)
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U1_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55A_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → U3_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55A_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → BALANCE55A_IN_GAAAAAAAAAGA(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)
BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55cA_in_gaaaaaaaaaga(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21))
U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55cA_out_gaaaaaaaaaga(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21)) → U9_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55A_in_gaaaaaaaaaga(X3, X13, X14, X22, X23, X24, X25, X15, X16, X21, X4, X26))
U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55cA_out_gaaaaaaaaaga(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21)) → BALANCE55A_IN_GAAAAAAAAAGA(X3, X13, X14, X22, X23, X24, X25, X15, X16, X21, X4, X26)
BALANCED_IN_GA(tree(X1, X2, X3), tree(X4, X5, X6)) → U10_GA(X1, X2, X3, X4, X5, X6, balance55cC_in_gaaaaaaaaaaaaga(X1, X7, X8, X9, X10, X11, X12, X4, X13, X5, X14, X6, X15, X2, X16))
U10_GA(X1, X2, X3, X4, X5, X6, balance55cC_out_gaaaaaaaaaaaaga(X1, X7, X8, X9, X10, X11, X12, X4, X13, X5, X14, X6, X15, X2, X16)) → U11_GA(X1, X2, X3, X4, X5, X6, balance55B_in_gaaaaaaa(X3, X9, X10, X7, X8, X11, X12, X16))
U10_GA(X1, X2, X3, X4, X5, X6, balance55cC_out_gaaaaaaaaaaaaga(X1, X7, X8, X9, X10, X11, X12, X4, X13, X5, X14, X6, X15, X2, X16)) → BALANCE55B_IN_GAAAAAAA(X3, X9, X10, X7, X8, X11, X12, X16)
BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) → U4_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55A_in_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21))
BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21)
BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) → U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21))
U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21)) → U6_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55B_in_gaaaaaaa(X3, X17, X18, X6, X7, X19, X20, X21))
U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21)) → BALANCE55B_IN_GAAAAAAA(X3, X17, X18, X6, X7, X19, X20, X21)

The TRS R consists of the following rules:

balance55cA_in_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7) → balance55cA_out_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7)
balance55cA_in_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cA_out_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20)
balance55cC_in_gaaaaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6) → balance55cC_out_gaaaaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6)
balance55cC_in_gaaaaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20) → U17_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25))
U17_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25)) → U18_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U18_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cC_out_gaaaaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55A_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55A_in_gaaaaaaaaaga(x1, x11)
balance55cA_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55cA_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55cC_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55cC_in_gaaaaaaaaaaaaga(x1, x14)
balance55cC_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55cC_out_gaaaaaaaaaaaaga(x1, x14)
U17_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U17_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
U18_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U18_gaaaaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55B_in_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  balance55B_in_gaaaaaaa(x1)
BALANCED_IN_GA(x1, x2)  =  BALANCED_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_GA(x1, x2, x3, x4, x5, x11)
BALANCE55A_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  BALANCE55A_IN_GAAAAAAAAAGA(x1, x11)
U1_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U1_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U3_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U3_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U8_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_GA(x1, x2, x3, x4, x5, x11)
U9_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_GA(x1, x2, x3, x4, x5, x11)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x7)
BALANCE55B_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  BALANCE55B_IN_GAAAAAAA(x1)
U4_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U4_GAAAAAAA(x1, x2, x3, x17)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U5_GAAAAAAA(x1, x2, x3, x17)
U6_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U6_GAAAAAAA(x1, x2, x3, x17)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → U7_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55A_in_gaaaaaaaaaga(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21))
BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21)
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U1_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55A_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → U3_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55A_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → BALANCE55A_IN_GAAAAAAAAAGA(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)
BALANCED_IN_GA(tree(tree(X1, X2, X3), X4, X5), tree(tree(X6, X7, X8), X9, X10)) → U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55cA_in_gaaaaaaaaaga(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21))
U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55cA_out_gaaaaaaaaaga(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21)) → U9_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55A_in_gaaaaaaaaaga(X3, X13, X14, X22, X23, X24, X25, X15, X16, X21, X4, X26))
U8_GA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, balance55cA_out_gaaaaaaaaaga(X1, X11, X12, X13, X14, X15, X16, .(','(X10, -(X17, [])), .(','(X6, -(X18, .(X7, X19))), .(','(X8, -(X19, .(X9, X17))), X20))), X20, X18, X2, X21)) → BALANCE55A_IN_GAAAAAAAAAGA(X3, X13, X14, X22, X23, X24, X25, X15, X16, X21, X4, X26)
BALANCED_IN_GA(tree(X1, X2, X3), tree(X4, X5, X6)) → U10_GA(X1, X2, X3, X4, X5, X6, balance55cC_in_gaaaaaaaaaaaaga(X1, X7, X8, X9, X10, X11, X12, X4, X13, X5, X14, X6, X15, X2, X16))
U10_GA(X1, X2, X3, X4, X5, X6, balance55cC_out_gaaaaaaaaaaaaga(X1, X7, X8, X9, X10, X11, X12, X4, X13, X5, X14, X6, X15, X2, X16)) → U11_GA(X1, X2, X3, X4, X5, X6, balance55B_in_gaaaaaaa(X3, X9, X10, X7, X8, X11, X12, X16))
U10_GA(X1, X2, X3, X4, X5, X6, balance55cC_out_gaaaaaaaaaaaaga(X1, X7, X8, X9, X10, X11, X12, X4, X13, X5, X14, X6, X15, X2, X16)) → BALANCE55B_IN_GAAAAAAA(X3, X9, X10, X7, X8, X11, X12, X16)
BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) → U4_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55A_in_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21))
BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21)
BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) → U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21))
U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21)) → U6_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55B_in_gaaaaaaa(X3, X17, X18, X6, X7, X19, X20, X21))
U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21)) → BALANCE55B_IN_GAAAAAAA(X3, X17, X18, X6, X7, X19, X20, X21)

The TRS R consists of the following rules:

balance55cA_in_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7) → balance55cA_out_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7)
balance55cA_in_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cA_out_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20)
balance55cC_in_gaaaaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6) → balance55cC_out_gaaaaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6)
balance55cC_in_gaaaaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20) → U17_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25))
U17_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25)) → U18_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U18_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cC_out_gaaaaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55A_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55A_in_gaaaaaaaaaga(x1, x11)
balance55cA_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55cA_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55cC_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55cC_in_gaaaaaaaaaaaaga(x1, x14)
balance55cC_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55cC_out_gaaaaaaaaaaaaga(x1, x14)
U17_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U17_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
U18_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U18_gaaaaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55B_in_gaaaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  balance55B_in_gaaaaaaa(x1)
BALANCED_IN_GA(x1, x2)  =  BALANCED_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U7_GA(x1, x2, x3, x4, x5, x11)
BALANCE55A_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  BALANCE55A_IN_GAAAAAAAAAGA(x1, x11)
U1_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U1_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U3_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U3_GAAAAAAAAAGA(x1, x2, x3, x19, x21)
U8_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U8_GA(x1, x2, x3, x4, x5, x11)
U9_GA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U9_GA(x1, x2, x3, x4, x5, x11)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x7)
BALANCE55B_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  BALANCE55B_IN_GAAAAAAA(x1)
U4_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U4_GAAAAAAA(x1, x2, x3, x17)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U5_GAAAAAAA(x1, x2, x3, x17)
U6_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U6_GAAAAAAA(x1, x2, x3, x17)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 13 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → BALANCE55A_IN_GAAAAAAAAAGA(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)

The TRS R consists of the following rules:

balance55cA_in_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7) → balance55cA_out_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7)
balance55cA_in_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cA_out_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20)
balance55cC_in_gaaaaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6) → balance55cC_out_gaaaaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6)
balance55cC_in_gaaaaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20) → U17_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25))
U17_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25)) → U18_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U18_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cC_out_gaaaaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55cA_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55cA_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55cC_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55cC_in_gaaaaaaaaaaaaga(x1, x14)
balance55cC_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55cC_out_gaaaaaaaaaaaaga(x1, x14)
U17_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U17_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
U18_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U18_gaaaaaaaaaaaaga(x1, x2, x3, x19, x26)
BALANCE55A_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  BALANCE55A_IN_GAAAAAAAAAGA(x1, x11)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U2_GAAAAAAAAAGA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → BALANCE55A_IN_GAAAAAAAAAGA(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)

The TRS R consists of the following rules:

balance55cA_in_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7) → balance55cA_out_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7)
balance55cA_in_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cA_out_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55cA_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55cA_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
BALANCE55A_IN_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  BALANCE55A_IN_GAAAAAAAAAGA(x1, x11)
U2_GAAAAAAAAAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U2_GAAAAAAAAAGA(x1, x2, x3, x19, x21)

We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X19) → U2_GAAAAAAAAAGA(X1, X2, X3, X19, balance55cA_in_gaaaaaaaaaga(X1, X2))
U2_GAAAAAAAAAGA(X1, X2, X3, X19, balance55cA_out_gaaaaaaaaaga(X1, X2)) → BALANCE55A_IN_GAAAAAAAAAGA(X3, X19)
BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X19) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X2)

The TRS R consists of the following rules:

balance55cA_in_gaaaaaaaaaga(nil, X6) → balance55cA_out_gaaaaaaaaaga(nil, X6)
balance55cA_in_gaaaaaaaaaga(tree(X1, X2, X3), X19) → U13_gaaaaaaaaaga(X1, X2, X3, X19, balance55cA_in_gaaaaaaaaaga(X1, X2))
U13_gaaaaaaaaaga(X1, X2, X3, X19, balance55cA_out_gaaaaaaaaaga(X1, X2)) → U14_gaaaaaaaaaga(X1, X2, X3, X19, balance55cA_in_gaaaaaaaaaga(X3, X19))
U14_gaaaaaaaaaga(X1, X2, X3, X19, balance55cA_out_gaaaaaaaaaga(X3, X19)) → balance55cA_out_gaaaaaaaaaga(tree(X1, X2, X3), X19)

The set Q consists of the following terms:

balance55cA_in_gaaaaaaaaaga(x0, x1)
U13_gaaaaaaaaaga(x0, x1, x2, x3, x4)
U14_gaaaaaaaaaga(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• U2_GAAAAAAAAAGA(X1, X2, X3, X19, balance55cA_out_gaaaaaaaaaga(X1, X2)) → BALANCE55A_IN_GAAAAAAAAAGA(X3, X19)
  The graph contains the following edges 3 >= 1, 4 >= 2

• BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X19) → BALANCE55A_IN_GAAAAAAAAAGA(X1, X2)
  The graph contains the following edges 1 > 1, 1 > 2

• BALANCE55A_IN_GAAAAAAAAAGA(tree(X1, X2, X3), X19) → U2_GAAAAAAAAAGA(X1, X2, X3, X19, balance55cA_in_gaaaaaaaaaga(X1, X2))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3, 2 >= 4

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) → U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21))
U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21)) → BALANCE55B_IN_GAAAAAAA(X3, X17, X18, X6, X7, X19, X20, X21)

The TRS R consists of the following rules:

balance55cA_in_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7) → balance55cA_out_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7)
balance55cA_in_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cA_out_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20)
balance55cC_in_gaaaaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6) → balance55cC_out_gaaaaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, .(','(X4, -(.(X5, X6), .(X7, X8))), .(','(X9, -(X8, [])), X10)), X10, X4, .(X5, X6), X7, X8, X9, X10, X5, X6)
balance55cC_in_gaaaaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20) → U17_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25))
U17_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, .(','(X16, -(X15, [])), .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18))), X18, X13, X2, X25)) → U18_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U18_gaaaaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cC_out_gaaaaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, tree(X10, X11, X12), X13, X14, X15, X16, .(','(X10, -(X13, .(X11, X17))), .(','(X12, -(X17, .(X14, X15))), X18)), X19, X20)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55cA_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55cA_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
balance55cC_in_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55cC_in_gaaaaaaaaaaaaga(x1, x14)
balance55cC_out_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15)  =  balance55cC_out_gaaaaaaaaaaaaga(x1, x14)
U17_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U17_gaaaaaaaaaaaaga(x1, x2, x3, x19, x21)
U18_gaaaaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U18_gaaaaaaaaaaaaga(x1, x2, x3, x19, x26)
BALANCE55B_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  BALANCE55B_IN_GAAAAAAA(x1)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U5_GAAAAAAA(x1, x2, x3, x17)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3), X4, X5, X6, X7, .(','(tree(X8, X9, X10), -(X11, X12)), X13), .(','(X8, -(X11, .(X9, X14))), .(','(X10, -(X14, X12)), X15)), X16) → U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21))
U5_GAAAAAAA(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X17, X18, X19, X20, X13, X15, X16, X2, X21)) → BALANCE55B_IN_GAAAAAAA(X3, X17, X18, X6, X7, X19, X20, X21)

The TRS R consists of the following rules:

balance55cA_in_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7) → balance55cA_out_gaaaaaaaaaga(nil, X1, .(','(nil, -(X2, X2)), X3), X2, X3, X4, X5, X4, X5, .(X6, X7), X6, X7)
balance55cA_in_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20) → U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_in_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25))
U13_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, balance55cA_out_gaaaaaaaaaga(X1, X4, X5, X21, X22, X23, X24, X15, X17, X18, X2, X25)) → U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_in_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20))
U14_gaaaaaaaaaga(X1, X2, X3, X4, X5, X6, X7, X8, X9, X10, X11, X12, X13, X14, X15, X16, X17, X18, X19, X20, X21, X22, X23, X24, X25, balance55cA_out_gaaaaaaaaaga(X3, X21, X22, X6, X7, X8, X9, X23, X24, X25, X19, X20)) → balance55cA_out_gaaaaaaaaaga(tree(X1, X2, X3), X4, X5, X6, X7, X8, X9, .(','(tree(X10, X11, X12), -(X13, X14)), X15), .(','(X10, -(X13, .(X11, X16))), .(','(X12, -(X16, X14)), X17)), X18, X19, X20)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
balance55cA_in_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_in_gaaaaaaaaaga(x1, x11)
nil  =  nil
balance55cA_out_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12)  =  balance55cA_out_gaaaaaaaaaga(x1, x11)
U13_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21)  =  U13_gaaaaaaaaaga(x1, x2, x3, x19, x21)
U14_gaaaaaaaaaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26)  =  U14_gaaaaaaaaaga(x1, x2, x3, x19, x26)
BALANCE55B_IN_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  BALANCE55B_IN_GAAAAAAA(x1)
U5_GAAAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17)  =  U5_GAAAAAAA(x1, x2, x3, x17)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3)) → U5_GAAAAAAA(X1, X2, X3, balance55cA_in_gaaaaaaaaaga(X1, X2))
U5_GAAAAAAA(X1, X2, X3, balance55cA_out_gaaaaaaaaaga(X1, X2)) → BALANCE55B_IN_GAAAAAAA(X3)

The TRS R consists of the following rules:

balance55cA_in_gaaaaaaaaaga(nil, X6) → balance55cA_out_gaaaaaaaaaga(nil, X6)
balance55cA_in_gaaaaaaaaaga(tree(X1, X2, X3), X19) → U13_gaaaaaaaaaga(X1, X2, X3, X19, balance55cA_in_gaaaaaaaaaga(X1, X2))
U13_gaaaaaaaaaga(X1, X2, X3, X19, balance55cA_out_gaaaaaaaaaga(X1, X2)) → U14_gaaaaaaaaaga(X1, X2, X3, X19, balance55cA_in_gaaaaaaaaaga(X3, X19))
U14_gaaaaaaaaaga(X1, X2, X3, X19, balance55cA_out_gaaaaaaaaaga(X3, X19)) → balance55cA_out_gaaaaaaaaaga(tree(X1, X2, X3), X19)

The set Q consists of the following terms:

balance55cA_in_gaaaaaaaaaga(x0, x1)
U13_gaaaaaaaaaga(x0, x1, x2, x3, x4)
U14_gaaaaaaaaaga(x0, x1, x2, x3, x4)

We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• U5_GAAAAAAA(X1, X2, X3, balance55cA_out_gaaaaaaaaaga(X1, X2)) → BALANCE55B_IN_GAAAAAAA(X3)
  The graph contains the following edges 3 >= 1

• BALANCE55B_IN_GAAAAAAA(tree(X1, X2, X3)) → U5_GAAAAAAA(X1, X2, X3, balance55cA_in_gaaaaaaaaaga(X1, X2))
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

(20) YES